﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using SimpleIR;
using System.Diagnostics.Contracts;

namespace RgnAnalyzer.Domain
{
	public partial class AProgramMemory
	{
		/// <summary>
		/// True if the state represented by this model is infeaseable (can never occour).
		/// </summary>
		private bool m_infeasableState; 
		
		/// <summary>
		/// A map from locals and statics to the <c>MNode</c> that represents the value of the name. 
		/// </summary>
		private readonly Dictionary<IRRootIdentifier, int> m_nametonodemap;

		/// <summary>
		/// A map from external references (and the parameter targets at call) to nodes in this..
		/// </summary>
		private readonly Dictionary<AExternalRef, int[]> m_externalrefs;

		/// <summary>
		/// A list of <c>SNode</c> objects representing the eval stack, grows from 0 up.
		/// </summary>
		private readonly List<AEvalStackEntry> m_evalstack; 

		/// <summary>
		/// All the nodes in the graph.
		/// </summary>
		private readonly List<ALocation> m_memory;
		
		[ContractInvariantMethod]
		private void PModelInvariant()
		{
			Contract.Invariant(this.m_nametonodemap != null);
			Contract.Invariant(this.m_externalrefs != null);
			Contract.Invariant(this.m_evalstack != null);

			Contract.Invariant(this.m_memory != null);
		}

		internal AProgramMemory()
		{
			this.m_infeasableState = false;
			this.m_nametonodemap = new Dictionary<IRRootIdentifier, int>();
			this.m_externalrefs = new Dictionary<AExternalRef, int[]>();
			this.m_evalstack = new List<AEvalStackEntry>();

			this.m_memory = new List<ALocation>();
		}

		internal static AProgramMemory MakeInfeasibleFlowProgMemory()
		{
			Contract.Ensures(Contract.Result<AProgramMemory>() != null);
			Contract.Ensures(Contract.Result<AProgramMemory>().IsInfeasable);

			AProgramMemory res = new AProgramMemory();
			res.SetInfeasable();
			return res;
		}

		private AProgramMemory(AProgramMemory pm)
		{
			Contract.Requires(pm != null);

			this.m_infeasableState = pm.m_infeasableState;
		
			this.m_memory = new List<ALocation>(pm.m_memory.Count);
			for(int i = 0; i < pm.m_memory.Count; ++i)
				this.m_memory.Add(pm.m_memory[i].CopyLocation());

			this.m_externalrefs = new Dictionary<AExternalRef, int[]>(pm.m_externalrefs.Count);
			foreach(KeyValuePair<AExternalRef, int[]> mnkvp in pm.m_externalrefs)
				this.m_externalrefs.Add(mnkvp.Key, (int[])mnkvp.Value.Clone());

			this.m_nametonodemap = new Dictionary<IRRootIdentifier, int>();
			foreach(KeyValuePair<IRRootIdentifier, int> rrid in pm.m_nametonodemap)
				this.m_nametonodemap.Add(rrid.Key, rrid.Value);

			this.m_evalstack = new List<AEvalStackEntry>(pm.m_evalstack);
		}

		internal AProgramMemory CopyMemoryState()
		{
			Contract.Ensures(Contract.Result<AProgramMemory>() != null);

			return new AProgramMemory(this);
		}

		/// <summary>
		/// Copy <c>pm</c> and assign it into this.
		/// </summary>
		internal void AssignIntoThis(AProgramMemory pm)
		{
			Contract.Requires(pm != null);

			this.m_infeasableState = pm.m_infeasableState;
		
			this.m_memory.Clear();
			for(int i = 0; i < pm.m_memory.Count; ++i)
				this.m_memory.Add(pm.m_memory[i].CopyLocation());

			this.m_externalrefs.Clear();
			foreach(KeyValuePair<AExternalRef, int[]> mnkvp in pm.m_externalrefs)
				this.m_externalrefs.Add(mnkvp.Key, (int[])mnkvp.Value.Clone());

			this.m_nametonodemap.Clear();
			foreach(KeyValuePair<IRRootIdentifier, int> rrid in pm.m_nametonodemap)
				this.m_nametonodemap.Add(rrid.Key, rrid.Value);

			this.m_evalstack.Clear();
			this.m_evalstack.AddRange(pm.m_evalstack);
		}

		/// <summary>
		/// Set the program model to the initial state at the start of the program given the list of static var pairs.
		/// </summary>
		internal void IntialStateProgModel(List<IRStaticField> staticVars)
		{
			Contract.Requires(!this.IsInfeasable);
			Contract.Requires(staticVars != null && (!staticVars.Contains(null)));

			IRClassType strarrayclass = (IRClassType)GlobalAnalysisState.TProg.TypeTable.LookupTypeForName("System.String[]");
			IRPtrType strarrayptr = GlobalAnalysisState.TProg.TypeTable.LookupPointerTypeFor(strarrayclass);

			AHomeLocation sn = this.AddArgOrStaticVar(GlobalAnalysisState.TProg.NameTable.LookupLocalVarName("args"), strarrayptr, 0);
			AObject sa = this.AllocateStringArray(0);

			APossiblePointerTarget ppt = new APossiblePointerTarget(sa.Address);
			sn.DoGeneralWriteToLocation_SingleTrgt(IRBasicAccessPath.EmptyAccessPath, ppt, true, true, 0);

			foreach(IRStaticField sf in staticVars)
				this.AddArgOrStaticVar(sf, sf.FieldType, 0);
		}

		/// <summary>
		/// Compute the PIModel representation of this graph for further inspection, analysis, and display operations.
		/// </summary>
		public PInfoModel.PIModel MakePIModelForThis()
		{
			PInfoModel.PIModel pim = new PInfoModel.PIModel();

			if(this.m_infeasableState)
				return null;

			Dictionary<ALocation, List<PInfoModel.PIExternalRef>> extrmap = new Dictionary<ALocation, List<PInfoModel.PIExternalRef>>();
			foreach(KeyValuePair<AExternalRef, int[]> extkvp in this.m_externalrefs)
			{
				for(int i = 0; i < extkvp.Value.Length; ++i)
				{
					ALocation tn = this.m_memory[extkvp.Value[i]];
					if(!extrmap.ContainsKey(tn))
						extrmap.Add(tn, new List<PInfoModel.PIExternalRef>());
					extrmap[tn].Add(new PInfoModel.PIExternalRef(extkvp.Key.IDTAG, extkvp.Key.StaticRef));
				}
			}

			Dictionary<ALocation, IRRootIdentifier> homelocs = new Dictionary<ALocation, IRRootIdentifier>();
			foreach(KeyValuePair<IRRootIdentifier, int> rrid in this.m_nametonodemap)
				homelocs.Add(this.m_memory[rrid.Value], rrid.Key);

			//add all the nodes
			foreach(ALocation n in this.m_memory)
			{
				int[] identity = (n.IdentityTags.Length == 0) ? PInfoModel.PIMNode.EmptyIdentities : (int[])n.IdentityTags.Clone();

				PInfoModel.PIUseMod[] umv;
				if(n.UMInfo.Count == 0)
					umv = PInfoModel.PIMNode.EmptyUseMod;
				else
				{
					umv = new PInfoModel.PIUseMod[n.UMInfo.Count];
					for(int i = 0; i < n.UMInfo.Count; ++i)
						umv[i] = new PInfoModel.PIUseMod((PInfoModel.PIUseMod.Value)n.UMInfo[i].UMTag, n.UMInfo[i].UMLine, n.UMInfo[i].UMAccessPath);
					Array.Sort(umv);
				}

				PInfoModel.PIEscapeSite[] escape;
				if(n.AllocationEscapeSites.Length == 0)
					escape = PInfoModel.PIMNode.EmptyEscapes;
				else
				{
					escape = new PInfoModel.PIEscapeSite[n.AllocationEscapeSites.Length];
					for(int i = 0; i < n.AllocationEscapeSites.Length; ++i)
						escape[i] = new PInfoModel.PIEscapeSite(n.AllocationEscapeSites[i].EscapeLine, n.AllocationEscapeSites[i].EscapeLoopFlow, n.AllocationEscapeSites[i].EscapeIdentity);
					Array.Sort(escape);
				}

				IRRootIdentifier homeloc = (homelocs.ContainsKey(n) ? homelocs[n] : null);

				PInfoModel.PIExternalRef[] extr = (extrmap.ContainsKey(n) ? extrmap[n].ToArray() : PInfoModel.PIMNode.EmptyExtRefs);
				Array.Sort(extr);

				bool mempty = (n is AContainer && ((AContainer)n).MustBeEmpty);
				PInfoModel.PIMNode pin = new PInfoModel.PIMNode(n.Address, n.LocationType, homeloc, umv, identity, n.IsUniqueLocation(), escape, PInfoModel.PIMNode.EmptyEdges, new List<PInfoModel.PIMEdge>(), extr, mempty);
				pim.Nodes.Add(pin);
			}

			//add the external refs
			foreach(KeyValuePair<AExternalRef, int[]> extkvp in this.m_externalrefs)
				pim.AddExternalRefTrgets(new PInfoModel.PIExternalRef(extkvp.Key.IDTAG, extkvp.Key.StaticRef), (int[])extkvp.Value.Clone());

			//add the var refs
			foreach(KeyValuePair<IRRootIdentifier, int> rrid in this.m_nametonodemap)
				pim.AddRootIdentifierHome(rrid.Key, rrid.Value);

			//add the eval stack
			for(int i = 0; i < this.m_evalstack.Count; ++i)
			{
				AEvalStackEntry sn = this.m_evalstack[i];
				PInfoModel.PIMEdge[] trgts;
				if(sn.SLocType is IRPrimitiveType)
					trgts = PInfoModel.PISNode.EmptyTrgts;
				else if(sn.SLocType is IRReferenceType)
				{
					AReference rr = sn.ReferenceValue;
					trgts = new PInfoModel.PIMEdge[rr.RTargetCount];
					for(int j = 0; j < rr.RTargetCount; ++j)
					{
						APossibleReferenceTarget aprt = rr.GetIthPossibleRefTrgt(j);
						PInfoModel.PIMEdge ee = new PInfoModel.PIMEdge(true, i, IRBasicAccessPath.EmptyAccessPath, aprt.RTarget, aprt.TrgtOffset, true, rr.MustBeNonNull, "Unknown");
						trgts[j] = ee;
						pim.Nodes[ee.TargetAddress].InEdges.Add(ee);
					}
				}
				else
				{
					APtrValueMap pta = (sn.SLocType is IRPtrType ? sn.PointerValue : sn.StructValue);
					trgts = new PInfoModel.PIMEdge[pta.PTargetCount];
					for(int j = 0; j < pta.PTargetCount; ++j)
					{
						APossiblePointerTarget appt = pta.PTargets[j];
						bool mustnonnull = pta.PathMustNonNull(appt.SourceOffset);

						PInfoModel.PIMEdge ee = new PInfoModel.PIMEdge(true, i, appt.SourceOffset, appt.PTarget, IRBasicAccessPath.EmptyAccessPath, appt.IsInjective, mustnonnull, AIndexPosition.ConvertToString(appt.IndexPosFlag));
						trgts[j] = ee;
						pim.Nodes[ee.TargetAddress].InEdges.Add(ee);
					}
				}

				PInfoModel.PISNode nsn = new PInfoModel.PISNode(sn.SLocType, trgts);
				pim.EvalStack.Add(nsn);
			}

			//add the heap edges
			foreach(ALocation n in this.m_memory)
			{
				if(n.LocationType is IRPrimitiveType)
				{ ;}
				else if(n.LocationType is IRReferenceType)
				{
					AReference rr = ((AHomeLocation)n).ReferenceValue;
					for(int j = 0; j < rr.RTargetCount; ++j)
					{
						APossibleReferenceTarget aprt = rr.GetIthPossibleRefTrgt(j);
						PInfoModel.PIMEdge ee = new PInfoModel.PIMEdge(false, n.Address, IRBasicAccessPath.EmptyAccessPath, aprt.RTarget, aprt.TrgtOffset, rr.MustBeNonNull, true, "Unknown");
						pim.Nodes[n.Address].AddOutEdge(ee);
						pim.Nodes[ee.TargetAddress].InEdges.Add(ee);
					}
				}
				else if(n.LocationType is IRPtrType)
				{
					APtrValueMap pta = ((AHomeLocation)n).PointerValue;
					for(int j = 0; j < pta.PTargetCount; ++j)
					{
						APossiblePointerTarget appt = pta.PTargets[j];
						bool mustnonnull = pta.PathMustNonNull(appt.SourceOffset);

						PInfoModel.PIMEdge ee = new PInfoModel.PIMEdge(false, n.Address, appt.SourceOffset, appt.PTarget, IRBasicAccessPath.EmptyAccessPath, appt.IsInjective, mustnonnull, AIndexPosition.ConvertToString(appt.IndexPosFlag));
						pim.Nodes[n.Address].AddOutEdge(ee);
						pim.Nodes[ee.TargetAddress].InEdges.Add(ee);
					}
				}
				else
				{
					APtrValueMap pta = n.StructOrClassPointers;
					for(int j = 0; j < pta.PTargetCount; ++j)
					{
						APossiblePointerTarget appt = pta.PTargets[j];
						bool mustnonnull = pta.PathMustNonNull(appt.SourceOffset);

						PInfoModel.PIMEdge ee = new PInfoModel.PIMEdge(false, n.Address, appt.SourceOffset, appt.PTarget, IRBasicAccessPath.EmptyAccessPath, appt.IsInjective, mustnonnull, AIndexPosition.ConvertToString(appt.IndexPosFlag));
						pim.Nodes[n.Address].AddOutEdge(ee);
						pim.Nodes[ee.TargetAddress].InEdges.Add(ee);
					}
				}
			}

			return pim;
		}

		/// <summary>
		/// Tidy up the summary states for completing the info.
		/// </summary>
		internal static void FinalInfoComputeTidyInOutSummaries(AProgramMemory sin, AProgramMemory sout,
			Dictionary<int, int> idsimplifymap, Dictionary<AExternalRef, AExternalRef> extrsimplifymap,
			Dictionary<PInfoModel.PIExternalRef, HashSet<PInfoModel.PIExternalRef>> erremap, Dictionary<int, HashSet<int>> idremap)
		{
			//first compute the fresh values and mappings based on the input model
			Dictionary<int, List<AExternalRef>> erfmap = new Dictionary<int, List<AExternalRef>>();
			foreach(KeyValuePair<AExternalRef, int[]> ekvp in sin.m_externalrefs)
			{
				for(int i = 0; i < ekvp.Value.Length; ++i)
				{
					if(!erfmap.ContainsKey(ekvp.Value[i]))
						erfmap.Add(ekvp.Value[i], new List<AExternalRef>());
					erfmap[ekvp.Value[i]].Add(ekvp.Key);
				}
			}
			sin.m_externalrefs.Clear();

			for(int i = 0; i < sin.m_memory.Count; ++i)
			{
				ALocation ll = sin.m_memory[i];
				HashSet<int> oldids = new HashSet<int>(ll.IdentityTags);
				ll.UniqueifyIdentityTags();
				int newtag = ll.IdentityTags[0];

				idremap.Add(newtag, oldids);
				foreach(int ii in oldids)
					idsimplifymap.Add(ii, newtag);

				if(erfmap.ContainsKey(i))
				{
					AExternalRef ner = AExternalRef.ComputeSummaryAExternalRef(erfmap[i]);
					sin.m_externalrefs.Add(ner, new int[] { i });

					PInfoModel.PIExternalRef pir = new PInfoModel.PIExternalRef(ner.IDTAG, ner.StaticRef);
					HashSet<PInfoModel.PIExternalRef> rrfs = new HashSet<PInfoModel.PIExternalRef>();
					foreach(AExternalRef oer in erfmap[i])
					{
						PInfoModel.PIExternalRef rrpr = new PInfoModel.PIExternalRef(oer.IDTAG, oer.StaticRef);
						extrsimplifymap.Add(oer, ner);
						rrfs.Add(rrpr);
					}

					erremap.Add(pir, rrfs);
				}
			}

			//now apply the needed maps to the output model
			if(sout != null)
				sout.FinalInfoComputeTidySummary(idsimplifymap, extrsimplifymap);
		}

		/// <summary>
		/// Tidy up the summary states for completing the info.
		/// </summary>
		internal void FinalInfoComputeTidySummary(Dictionary<int, int> idsimplifymap, Dictionary<AExternalRef, AExternalRef> extrsimplifymap)
		{
			for(int i = 0; i < this.m_memory.Count; ++i)
			{
				ALocation ll = this.m_memory[i];
				HashSet<int> rmpids = new HashSet<int>();
				foreach(int ii in ll.IdentityTags)
					rmpids.Add(idsimplifymap[ii]);

				int[] ida;
				if(rmpids.Count == 0)
					ida = ALocation.EmptyIdentity;
				else
				{
					ida = new int[rmpids.Count];
					rmpids.CopyTo(ida);
					Array.Sort(ida);
				}

				ll.SetIDTagsForFinalProcessInfo(ida);
			}

			Dictionary<AExternalRef, HashSet<int>> ners = new Dictionary<AExternalRef, HashSet<int>>();
			foreach(KeyValuePair<AExternalRef, int[]> kvpp in this.m_externalrefs)
			{
				AExternalRef remapr = extrsimplifymap[kvpp.Key];
				if(!ners.ContainsKey(remapr))
					ners.Add(remapr, new HashSet<int>());
				ners[remapr].UnionWith(kvpp.Value);
			}
			this.m_externalrefs.Clear();

			foreach(KeyValuePair<AExternalRef, HashSet<int>> nkvpp in ners)
			{
				int[] ta = new int[nkvpp.Value.Count];
				nkvpp.Value.CopyTo(ta);

				this.m_externalrefs.Add(nkvpp.Key, ta);
			}
		}

		/// <summary>
		/// Return true if this model represents an infeasible flow state.
		/// </summary>
		public bool IsInfeasable 
		{ get { return this.m_infeasableState; } }

		/// <summary>
		/// Set this model to represent an infeasible flow state.
		/// </summary>
		internal void SetInfeasable()
		{
			this.m_infeasableState = true;

			this.m_nametonodemap.Clear();
			this.m_externalrefs.Clear();
			this.m_evalstack.Clear();

			this.m_memory.Clear();
		}

		/// <summary>
		/// Return a list of all the nodes in this were the node with a given id <c>k</c> is at index <c>k</c> in the list.
		/// DO NOT MODIFY THIS.
		/// </summary>
		internal List<ALocation> Memory
		{ get { return this.m_memory; } }

		/// <summary>
		/// Clear dead and no longer used variables as needed, and add newly inscope vars.
		/// Note this may leave some dangling nodes that previously contained the contents of the variables so until you normalize
		/// this may be a bit odd.
		/// </summary>
		/// <param name="liveAfter">Sorted List of vars in scope after this stmt.</param>
		internal void ClearVarsNotInScopeAddNew(HashSet<IRVarName> inscope, HashSet<IRVarName> liveatentry, Dictionary<IRVarName, IRType> nametotypemap, int line)
		{
			Contract.Requires(!this.IsInfeasable);
			Contract.Requires(inscope != null);
			Contract.Requires(liveatentry != null);
			Contract.Requires(nametotypemap != null);

			List<IRVarName> toelim = new List<IRVarName>();
			foreach(IRRootIdentifier rrp in this.m_nametonodemap.Keys)
			{
				if(rrp is IRVarName && (!inscope.Contains((IRVarName)rrp)))
					toelim.Add((IRVarName)rrp);
			}

			for(int i = 0; i < toelim.Count; ++i)
				this.m_nametonodemap.Remove(toelim[i]);

			foreach(IRVarName rri in inscope)
			{
				if(this.m_nametonodemap.ContainsKey(rri) && (!liveatentry.Contains(rri)))
				{
					AHomeLocation lvn = this.ResolveLocalGlobalTarget(rri);
					lvn.ClearDeadLocation();
				}

				if(!this.m_nametonodemap.ContainsKey(rri))
				{
					IRType lvt = nametotypemap[rri];

					int caddr = this.m_memory.Count;
					AHomeLocation loc;
					if(lvt is IRNumericType)
						loc = new AHomeLocation((IRNumericType)lvt, caddr, false, ZeroOne.Value.Zero, line);
					else if(lvt is IREnumType)
						loc = new AHomeLocation((IREnumType)lvt, caddr, false, ZeroOne.Value.Zero, line);
					else if(lvt is IRPtrType)
						loc = new AHomeLocation((IRPtrType)lvt, caddr, false, APtrValueMap.MakeInitalPtrValueMapPtr(), line);
					else if(lvt is IRReferenceType)
						loc = new AHomeLocation((IRReferenceType)lvt, caddr, false, AReference.CreateDefaultNullReference((IRReferenceType)lvt), line);
					else
						loc = new AHomeLocation((IRStructType)lvt, caddr, false, APtrValueMap.MakeInitalPtrValueMapComposite(lvt.TypeDescription.AllTerminalAccessPaths), line);

					this.m_nametonodemap.Add(rri, loc.Address);
					this.m_memory.Add(loc);
				}
			}
		}

		/// <summary>
		/// Clear out any variables that are not in scope going back around for the loop exit.
		/// </summary>
		internal void ClearVarsNotInScope_LoopHeadFinalProcess(HashSet<IRVarName> inscope, HashSet<IRVarName> liveatentry)
		{
			Contract.Requires(!this.IsInfeasable);
			Contract.Requires(inscope != null);
			Contract.Requires(liveatentry != null);
			
			HashSet<IRVarName> toelim = new HashSet<IRVarName>();
			foreach(IRRootIdentifier rrp in this.m_nametonodemap.Keys)
			{
				if(rrp is IRVarName && (!inscope.Contains((IRVarName)rrp)))
					toelim.Add((IRVarName)rrp);
			}

			foreach(IRVarName rri in inscope)
			{
				if(this.m_nametonodemap.ContainsKey(rri) && (!liveatentry.Contains(rri)))
					toelim.Add(rri);
			}

			foreach(IRVarName vvn in toelim)
				this.m_nametonodemap.Remove(vvn);
		}

		/// <summary>
		/// Add a fixed allocation site for a local or static name.
		/// </summary>
		private AHomeLocation AddArgOrStaticVar(IRRootIdentifier v, IRType tt, int line)
		{
			Contract.Requires(!this.IsInfeasable);
			Contract.Requires(v != null);
			Contract.Requires(tt != null);
			Contract.Ensures(Contract.Result<AHomeLocation>() != null);

			int caddr = this.m_memory.Count;
			bool isglobal = v is IRStaticField;

			AHomeLocation loc;
			if(tt is IRNumericType)
				loc = new AHomeLocation((IRNumericType)tt, caddr, isglobal, ZeroOne.Value.Zero, line);
			else if(tt is IREnumType)
				loc = new AHomeLocation((IREnumType)tt, caddr, isglobal, ZeroOne.Value.Zero, line);
			else if(tt is IRPtrType)
				loc = new AHomeLocation((IRPtrType)tt, caddr, isglobal, APtrValueMap.MakeInitalPtrValueMapPtr(), line);
			else if(tt is IRReferenceType)
				loc = new AHomeLocation((IRReferenceType)tt, caddr, isglobal, AReference.CreateDefaultNullReference((IRReferenceType)tt), line);
			else
				loc = new AHomeLocation((IRStructType)tt, caddr, isglobal, APtrValueMap.MakeInitalPtrValueMapComposite(tt.TypeDescription.AllTerminalAccessPaths), line);

			this.m_nametonodemap.Add(v, loc.Address);
			this.m_memory.Add(loc);

			return loc;
		}

		/// <summary>
		/// Peek at the top value from the eval stack.
		/// </summary>
		internal AEvalStackEntry EvalStackPeek()
		{
			if(this.m_evalstack.Count == 0)
				DebugReport.ReportError("Peek on empty eval stack.");

			return this.m_evalstack[this.m_evalstack.Count - 1];
		}

		/// <summary>
		/// Peek at the top value from the eval stack.
		/// </summary>
		internal AEvalStackEntry EvalStackPeekK(int k)
		{
			if(this.m_evalstack.Count <= k)
				DebugReport.ReportError("Peek past bottom of stack.");

			return this.m_evalstack[this.m_evalstack.Count - (k + 1)];
		}

		/// <summary>
		/// Remove the top value from the eval stack.
		/// </summary>
		internal AEvalStackEntry EvalStackPopWVal()
		{
			if(this.m_evalstack.Count == 0)
				DebugReport.ReportError("Pop on empty eval stack.");

			AEvalStackEntry val = this.m_evalstack[this.m_evalstack.Count - 1];
			this.m_evalstack.RemoveAt(this.m_evalstack.Count - 1);
			return val;
		}

		/// <summary>
		/// Remove the top value from the eval stack.
		/// </summary>
		internal void EvalStackPop()
		{
			if(this.m_evalstack.Count == 0)
				DebugReport.ReportError("Pop on empty eval stack.");

			this.m_evalstack.RemoveAt(this.m_evalstack.Count - 1);
		}

		/// <summary>
		/// Push to this node on the top of the eval stack.
		/// </summary>
		internal void EvalStackPush(AEvalStackEntry val)
		{ this.m_evalstack.Add(val); }

		/// <summary>
		/// Push to this node on the top of the eval stack.
		/// </summary>
		internal void EvalStackPush(IRNumericType evpt, ZeroOne.Value val)
		{
			if(evpt is IRFloatingPointType)
				this.m_evalstack.Add(AEvalStackEntry.MakeNumericStackEntry(GlobalAnalysisState.TProg.TypeTable.NumericStackValueType, ZeroOne.Value.Unknown));
			else
				this.m_evalstack.Add(AEvalStackEntry.MakeNumericStackEntry(GlobalAnalysisState.TProg.TypeTable.NumericStackValueType, val));
		}

		/// <summary>
		/// Push to this node on the top of the eval stack.
		/// </summary>
		internal void EvalStackPush(IREnumType evpt, ZeroOne.Value val)
		{ this.m_evalstack.Add(AEvalStackEntry.MakeNumericStackEntry(GlobalAnalysisState.TProg.TypeTable.NumericStackValueType, val)); }

		/// <summary>
		/// Push to this node on the top of the eval stack.
		/// </summary>
		internal void EvalStackPush(IRFunctionPointerType fptype, IRInvokeIdentity val)
		{ this.m_evalstack.Add(AEvalStackEntry.MakeFunctionPtrStackEntry(fptype, val)); }

		/// <summary>
		/// Push to this node on the top of the eval stack.
		/// </summary>
		internal void EvalStackPush(IRReferenceType reft, AReference rr)
		{ this.m_evalstack.Add(AEvalStackEntry.MakeReferenceStackEntry(reft, rr)); }

		/// <summary>
		/// Push to this node on the top of the eval stack.
		/// </summary>
		internal void EvalStackPush(IRPtrType ptrt, APtrValueMap pt)
		{ this.m_evalstack.Add(AEvalStackEntry.MakePtrStackEntry(ptrt, pt)); }

		/// <summary>
		/// Push to this node on the top of the eval stack.
		/// </summary>
		internal void EvalStackPush(IRPtrType ptrt, APossiblePointerTarget spt, bool mustnonnull)
		{ this.m_evalstack.Add(AEvalStackEntry.MakePtrStackEntry(ptrt, APtrValueMap.MakePtrWSingleTarget(spt, mustnonnull))); }

		/// <summary>
		/// Push to this node on the top of the eval stack.
		/// </summary>
		internal void EvalStackPush(IRStructType structtype, APtrValueMap strv)
		{ this.m_evalstack.Add(AEvalStackEntry.MakeStructStackEntry(structtype, strv)); }

		////////////////////

		/// <summary>
		/// Resolve the location for a local or global variable.
		/// </summary>
		internal ALocation ResolveRawAddress(int address)
		{ return this.m_memory[address]; }

		/// <summary>
		/// Resolve the location for a local or global variable.
		/// </summary>
		internal AHomeLocation ResolveLocalGlobalTarget(IRRootIdentifier var)
		{
			Contract.Requires(var != null);
			Contract.Ensures(Contract.Result<AHomeLocation>() != null);

			return (AHomeLocation)this.m_memory[this.m_nametonodemap[var]];
		}

		/// <summary>
		/// Resolve the location that the pointer is to.
		/// </summary>
		internal AObject ResolvePointerTarget(APossiblePointerTarget p)
		{
			Contract.Requires(p != null);
			Contract.Ensures(Contract.Result<AObject>() != null);

			return (AObject)this.m_memory[p.PTarget];
		}

		/// <summary>
		/// Resolve the location that the reference is to.
		/// </summary>
		internal ALocation ResolveReferenceTarget(APossibleReferenceTarget r)
		{
			Contract.Requires(r != null);
			Contract.Ensures(Contract.Result<ALocation>() != null);

			return this.m_memory[r.RTarget];
		}

		/// <summary>
		/// Allocate String[] Strings, for main and other locations.
		/// </summary>
		internal AObject AllocateStringArray(int line)
		{
			Contract.Requires(!this.IsInfeasable);
			Contract.Ensures(Contract.Result<AObject>() != null);

			IRContainerType strat = (IRContainerType)GlobalAnalysisState.TProg.TypeTable.LookupTypeForName("System.String[]");
			IRPtrType strarrptr = GlobalAnalysisState.TProg.TypeTable.LookupPointerTypeFor(strat);
			AContainer sarrloc = AContainer.AllocateContainerOfType(this.m_memory, strat, line);
			AObject sloc = AObject.AllocateObjectOfType(this.m_memory, GlobalAnalysisState.TProg.TypeTable.StringObjectType, line);
			sloc.MakeMultiLoc(); //may be many strings

			IRMemberField contf = strat.ContentsField;
			IRBasicAccessPath cbap = GlobalAnalysisState.TProg.GetAccessPathForSingleField(contf);
			APtrValueMap pvals = APtrValueMap.MakePtrWSingleTarget(new APossiblePointerTarget(sloc.Address), true);
			sarrloc.DoContainerContentsWriteToLocationBI(cbap, pvals, line, contf);

			return sarrloc;
		}

		////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		//Implementation of the abstract operations

		//////////////
		//Control Flow

		/// <summary>
		/// Help for simulating true/false branches, return the tuple of models (whentrue, whenfalse)
		/// </summary>
		internal Tuple<AProgramMemory, AProgramMemory> SplitOnExpTruthBoolVal()
		{
			Contract.Requires(!this.IsInfeasable);

			AEvalStackEntry sn = this.EvalStackPopWVal();

			if(sn.NumericValue == ZeroOne.Value.One)
				return new Tuple<AProgramMemory, AProgramMemory>(this, null);
			else if(sn.NumericValue == ZeroOne.Value.Zero)
				return new Tuple<AProgramMemory, AProgramMemory>(null, this);
			else
			{
				AProgramMemory fpm = this.CopyMemoryState();
				AProgramMemory tpm = this;
				return new Tuple<AProgramMemory, AProgramMemory>(tpm, fpm);
			}
		}

		/// <summary>
		/// Help for simulating switches, pop the control value and clone the state as needed.
		/// </summary>
		internal AProgramMemory[] SplitForSwitch(int trgtcount)
		{
			Contract.Requires(!this.IsInfeasable);

			this.EvalStackPop();

			AProgramMemory[] res = new AProgramMemory[trgtcount];
			for(int i = 1; i < trgtcount; ++i)
				res[i] = this.CopyMemoryState();
			res[0] = this;

			return res;
		}

		/// <summary>
		/// Advance the loop index info
		/// </summary>
		internal void SetStackTopAsLoopTraverseCurrent(IRVarName root, IRMemberField optf, IRVarName optindex, int loopmin, int loopmax, int indexpos, 
			bool indexget, bool enumcontget, bool enumdictget, bool enumdictkeyget, bool enumdictvalget)
		{
			AObject oc = this.GetTargetTraverseContainerWithCheck(root, optf, loopmin, loopmax);
			if(oc == null || oc.HasLocationBeenModInLoopWOptScalarCheck(loopmin, loopmax, false, -1))
				return;

			if(optindex != null && this.ResolveLocalGlobalTarget(optindex).HasLocationBeenModInLoopWOptScalarCheck(loopmin, loopmax, false, indexpos))
				return;

			APtrValueMap appt = oc.StructOrClassPointers;
			bool contok = ((IRContainerType)oc.LocationType).ContainerContentsType is IRPtrType;
			bool keyok = (oc.LocationType is IRDictionaryType) && (((IRKeyValuePairType)((IRDictionaryType)oc.LocationType).ContainerContentsType).KeyField.FieldType is IRPtrType);
			bool valok = (oc.LocationType is IRDictionaryType) && (((IRKeyValuePairType)((IRDictionaryType)oc.LocationType).ContainerContentsType).ValueField.FieldType is IRPtrType);

			for(int i = 0; i < appt.PTargetCount; ++i)
			{
				//we need to check the type of the container
				if(indexget || enumcontget)
				{
					if(appt.PTargets[i].SourceOffset.AccessPathHasSummaryLocation)
						contok &= appt.PTargets[i].IsInjective;
				}
				else if(enumdictget || enumdictkeyget || enumdictvalget)
				{
					if(appt.PTargets[i].SourceOffset.AccessPathHasSummaryLocation && appt.PTargets[i].SourceOffset.PathLast.FieldName.Equals("key"))
						keyok &= appt.PTargets[i].IsInjective;

					if(appt.PTargets[i].SourceOffset.AccessPathHasSummaryLocation && appt.PTargets[i].SourceOffset.PathLast.FieldName.Equals("value"))
						valok &= appt.PTargets[i].IsInjective;
				}
			}

			if((!contok) & (!keyok) & (!valok))
				return;

			IRBasicAccessPath okcontbap = (contok ? IRBasicAccessPath.EmptyAccessPath : null);
			IRBasicAccessPath okkeybap = (keyok ? GlobalAnalysisState.TProg.GetAccessPathForSingleField(((IRKeyValuePairType)((IRDictionaryType)oc.LocationType).ContainerContentsType).KeyField) : null);
			IRBasicAccessPath okvalbap = (valok ? GlobalAnalysisState.TProg.GetAccessPathForSingleField(((IRKeyValuePairType)((IRDictionaryType)oc.LocationType).ContainerContentsType).ValueField) : null);

			AEvalStackEntry evse = this.EvalStackPopWVal();
			APtrValueMap nppt = evse.PointerValue.InitializeLoopPositionInfoAs(AIndexPosition.Value.Current, okcontbap, okkeybap, okvalbap);
			this.EvalStackPush(AEvalStackEntry.MakePtrStackEntry((IRPtrType)evse.SLocType, nppt));
		}

		/// <summary>
		/// At a loop header update the allocation flow and usemod flow info to the "previous" loop iteration values.
		/// </summary>
		internal void AdvanceUseModAndAllocInfoToLoopPrevious(int loopminpos, int loopmaxpos, int loopprevpos)
		{
			for(int i = 0; i < this.m_memory.Count; ++i)
				this.m_memory[i].AdvanceUseModAndAllocInfoToLoopPrevious(loopminpos, loopmaxpos, loopprevpos);
		}

		/// <summary>
		/// Advance the loop index info
		/// </summary>
		internal void AdvanceLoopPositionInfo(IRVarName root, IRMemberField optf, IRVarName optindex, int loopmin, int loopmax, int indexpos)
		{
			bool oktoadv = this.CheckModForLoopTraversal_ClearIfNeeded(root, optf, optindex, loopmin, loopmax, indexpos);

			if(oktoadv)
			{
				for(int i = 0; i < this.m_memory.Count; ++i)
					this.m_memory[i].AdvanceLoopPositionInfo();
			}
		}

		/// <summary>
		/// Clear all loop index info
		/// </summary>
		internal void ClearLoopPositionInfo()
		{
			for(int i = 0; i < this.m_memory.Count; ++i)
				this.m_memory[i].ClearLoopPositionInfo();
		}

		/// <summary>
		/// Check if the needed pointers/index values have not been modified and that we are still cool for the loop traversal stuff.
		/// </summary>
		internal bool CheckModForLoopTraversal_ClearIfNeeded(IRVarName root, IRMemberField optf, IRVarName optindex, int loopmin, int loopmax, int indexpos)
		{
			AObject oc = this.GetTargetTraverseContainerWithCheck(root, optf, loopmin, loopmax);
			if(oc == null || oc.HasLocationBeenModInLoopWOptScalarCheck(loopmin, loopmax, false, -1))
			{
				this.ClearLoopPositionInfo();
				return false;
			}

			if(optindex != null && this.ResolveLocalGlobalTarget(optindex).HasLocationBeenModInLoopWOptScalarCheck(loopmin, loopmax, false, indexpos))
			{
				this.ClearLoopPositionInfo();
				return false;
			}

			return true;
		}

		/// <summary>
		/// Either get the target container that we are traversing or return null if some 
		/// part of the access path has been modified (or is ambig).
		/// </summary>
		private AObject GetTargetTraverseContainerWithCheck(IRVarName root, IRMemberField optf, int loopmin, int loopmax)
		{
			Contract.Requires(root != null);
			Contract.Ensures(Contract.Result<AObject>() == null || Contract.Result<AObject>().LocationType is IRContainerType);

			AHomeLocation vloc = this.ResolveLocalGlobalTarget(root);
			if(vloc.LocationType is IRReferenceType)
			{
				IRType rrt = ((IRReferenceType)vloc.LocationType).ReferenceTargetType;
				if((!(rrt is IRStructType)) || (!(rrt is IREnumeratorType)))
					return null;

				IREnumeratorType etype = (IREnumeratorType)rrt;
				ALocation llc = this.DoReadFromLocation_CheckSingleValuedNoMark(vloc, etype.EnumCollectionField);
				if(llc == null || vloc.HasLocationBeenModInLoopWOptScalarCheck(loopmin, loopmax, true, -1))
					return null;

				return (AObject)llc;
			}
			else if(vloc.LocationType is IRPtrType)
			{
				ALocation ll = this.DoReadFromLocation_CheckSingleValuedNoMark(vloc, null);
				if(ll == null || vloc.HasLocationBeenModInLoopWOptScalarCheck(loopmin, loopmax, true, -1))
					return null;

				//if this variable points to an enumerator then resolve through that otherwise check if we have another field 
				if(ll.LocationType is IRBoxedType)
				{
					IRMemberField boxf = ((IRBoxedType)ll.LocationType).BoxedValueField;
					IRValueType boxty = (IRValueType)boxf.FieldType;

					if(!(boxty is IREnumeratorType))
						return null;

					IREnumeratorType etype = (IREnumeratorType)boxty;
					ALocation llc = this.DoReadFromLocation_CheckSingleValuedNoMark(ll, etype.EnumCollectionField);
					if(llc == null || ll.HasLocationBeenModInLoopWOptScalarCheck(loopmin, loopmax, true, -1))
						return null;

					if(!(llc.LocationType is IRContainerType))
						return null;

					return (AObject)llc;
				}
				else if(optf != null)
				{
					ALocation llc = this.DoReadFromLocation_CheckSingleValuedNoMark(ll, optf);
					IRBasicAccessPath optfp = GlobalAnalysisState.TProg.GetAccessPathForSingleField(optf);
					if(llc == null || ll.HasLocationBeenModInLoopWOptScalarCheck(loopmin, loopmax, true, -1))
						return null;

					if(!(llc.LocationType is IRContainerType))
						return null;

					return (AObject)llc;
				}
				else
				{
					if(!(ll.LocationType is IRContainerType))
						return null;

					return (AObject)ll;
				}
			}
			else
			{
				return null;
			}
		}

		/// <summary>
		/// Do a read from the given location of the given field (null if the location is a variable).
		/// If there are multiple (or no) targets return null instead.
		/// </summary>
		private ALocation DoReadFromLocation_CheckSingleValuedNoMark(ALocation aloc, IRMemberField optf)
		{
			ALocation ll = null;
			IEnumerator<ATrgtEnum> aenum = aloc.GetTargetEnum();
			while(aenum.MoveNext())
			{
				if(optf == null)
				{
					if(ll != null)
						return null;
					ll = this.ResolveRawAddress(aenum.Current.TrgtAddress);
				}
				else if(aenum.Current.BAPPath.Path.Length >= 1 && aenum.Current.BAPPath.PathLast == optf)
				{
					if(ll != null)
						return null;
					ll = this.ResolveRawAddress(aenum.Current.TrgtAddress);
				}
				else
				{ ;}
			}

			return ll;
		}

		//////////////
		//Allocation

		/// <summary>
		/// Simulate the allocation of an object or struct (YOU MUST DO initialization call later if desired).
		/// Note we don't let you alloc raw pointers or blank arrays (because they always need a size parameter).
		/// </summary>
		internal void SimulateAllocBlank(IRType alloctype, int line)
		{
			Contract.Requires(alloctype != null);

			if(alloctype is IRStructType)
				this.EvalStackPush((IRStructType)alloctype, APtrValueMap.MakeInitalPtrValueMapComposite(alloctype.TypeDescription.AllTerminalAccessPaths));
			else
			{
				IRPtrType drftype = GlobalAnalysisState.TProg.TypeTable.LookupPointerTypeFor((IRClassType)alloctype);
				AObject nloc;

				if(alloctype is IRContainerType)
					nloc = AContainer.AllocateContainerOfType(this.m_memory, (IRContainerType)alloctype, line);
				else
					nloc = AObject.AllocateObjectOfType(this.m_memory, (IRClassType)alloctype, line);

				this.EvalStackPush(drftype, new APossiblePointerTarget(nloc.Address), true);
			}
		}

		/// <summary>
		/// Simulate the allocation of a delegate object.
		/// </summary>
		internal void SimulateAllocDelegate(IRLambdaType alloctype, int line)
		{
			Contract.Requires(alloctype != null);

			IRInvokeIdentity dsig = this.EvalStackPopWVal().FuncPtrValue;
			APtrValueMap closure = this.EvalStackPopWVal().PointerValue;
			ADelegate dd = ADelegate.AllocateDelegateOfType(this.m_memory, alloctype, closure, dsig, line);

			IRPtrType dpt = GlobalAnalysisState.TProg.TypeTable.LookupPointerTypeFor(alloctype);
			APossiblePointerTarget appt = new APossiblePointerTarget(dd.Address);
			this.EvalStackPush(dpt, appt, true);
		}

		//////////////
		//Primitive Load/Store

		/// <summary>
		/// Simulate the load of a value from a local variable to the stack.
		/// </summary>
		internal void SimulateLoadFromLocal(IRVarName rv, bool isdeadafterload, int line)
		{
			Contract.Requires(rv != null);

			AHomeLocation lvn = this.ResolveLocalGlobalTarget(rv);
			if(lvn.LocationType is IRNumericType | lvn.LocationType is IREnumType)
			{
				ZeroOne.Value val = lvn.ReadNumericFromViaName(line);
				if(lvn.LocationType is IRNumericType)
					this.EvalStackPush((IRNumericType)lvn.LocationType, val);
				else
					this.EvalStackPush((IREnumType)lvn.LocationType, val);
			}
			else if(lvn.LocationType is IRReferenceType)
			{
				AReference rr = lvn.ReadReferenceFromViaName(line);
				this.EvalStackPush((IRReferenceType)lvn.LocationType, rr);
			}
			else if(lvn.LocationType is IRPtrType)
			{
				APtrValueMap pvm = lvn.ReadPointerFromViaName(line);
				this.EvalStackPush((IRPtrType)lvn.LocationType, pvm);
			}
			else
			{
				Nullable<APtrValueMap> pvm = lvn.DoGeneralReadFromLocation(IRBasicAccessPath.EmptyAccessPath, line);
				this.EvalStackPush((IRStructType)lvn.LocationType, pvm.Value);
			}

			if(isdeadafterload)
				lvn.ClearDeadLocation();
		}

		/// <summary>
		/// Simulate the store of a value to a local variable from the stack.
		/// </summary>
		internal void SimulateStoreToLocal(IRVarName rv, int line)
		{
			Contract.Requires(rv != null);

			AEvalStackEntry evse = this.EvalStackPopWVal();
			AHomeLocation lvn = this.ResolveLocalGlobalTarget(rv);

			if(lvn.LocationType is IRNumericType | lvn.LocationType is IREnumType)
				lvn.WriteNumericToViaName(evse.NumericValue, line);
			else if(lvn.LocationType is IRReferenceType)
			{
				Contract.Assert(IRProgram.IsT1AssignableToT2(evse.SLocType, lvn.LocationType));

				lvn.WriteReferenceToViaName(evse.ReferenceValue, line);
			}
			else if(lvn.LocationType is IRPtrType)
			{
				Contract.Assert(IRProgram.IsT1AssignableToT2(evse.SLocType, lvn.LocationType));

				lvn.WritePointerToViaName(evse.PointerValue, line);
			}
			else
			{
				Contract.Assert(IRProgram.IsT1AssignableToT2(evse.SLocType, lvn.LocationType));

				lvn.DoGeneralWriteToLocation(IRBasicAccessPath.EmptyAccessPath, evse.StructValue, true, line);
			}
		}

		/// <summary>
		/// Simulate the load of a value from a global variable to the stack.
		/// </summary>
		internal void SimulateLoadFromGlobal(IRStaticField sf, int line)
		{
			Contract.Requires(sf != null);

			AHomeLocation lvn = this.ResolveLocalGlobalTarget(sf);
			if(lvn.LocationType is IRNumericType | lvn.LocationType is IREnumType)
			{
				ZeroOne.Value val = lvn.ReadNumericFromViaName(line);
				this.EvalStackPush((IRNumericType)lvn.LocationType, val);
			}
			else if(lvn.LocationType is IRPtrType)
			{
				APtrValueMap pvm = lvn.ReadPointerFromViaName(line);
				this.EvalStackPush((IRPtrType)lvn.LocationType, pvm);
			}
			else
			{
				Nullable<APtrValueMap> pvm = lvn.DoGeneralReadFromLocation(IRBasicAccessPath.EmptyAccessPath, line);
				this.EvalStackPush((IRPtrType)lvn.LocationType, pvm.Value);
			}
		}

		/// <summary>
		/// Simulate the store of a value to a global variable from the stack.
		/// </summary>
		internal void SimulateStoreToGlobal(IRStaticField sf, int line)
		{
			Contract.Requires(sf != null);

			AEvalStackEntry evse = this.EvalStackPopWVal();
			AHomeLocation gln = this.ResolveLocalGlobalTarget(sf);

			if(gln.LocationType is IRNumericType | gln.LocationType is IREnumType)
				gln.WriteNumericToViaName(evse.NumericValue, line);
			else if(gln.LocationType is IRPtrType)
			{
				Contract.Assert(IRProgram.IsT1AssignableToT2(evse.SLocType, sf.FieldType));

				gln.WritePointerToViaName(evse.PointerValue, line);
			}
			else
			{
				Contract.Assert(IRProgram.IsT1AssignableToT2(evse.SLocType, sf.FieldType));

				gln.DoGeneralWriteToLocation(IRBasicAccessPath.EmptyAccessPath, evse.StructValue, true, line);
			}
		}

		//////////////
		//Primitive Compare

		/// <summary>
		/// Simulate the equality operation.
		/// </summary>
		internal void SimulatePrimEQ()
		{
			ZeroOne.Value pn2 = this.EvalStackPopWVal().NumericValue;
			ZeroOne.Value pn1 = this.EvalStackPopWVal().NumericValue;

			ZeroOne.Value res = ZeroOne.Equal_Simulate(pn1, pn2);
			this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, res);
		}

		/// <summary>
		/// Simulate the less operation.
		/// </summary>
		internal void SimulateLess()
		{
			ZeroOne.Value pn2 = this.EvalStackPopWVal().NumericValue;
			ZeroOne.Value pn1 = this.EvalStackPopWVal().NumericValue;

			ZeroOne.Value res = ZeroOne.Less_Simulate(pn1, pn2);
			this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, res);
		}

		/// <summary>
		/// Simulate the less or equal operation.
		/// </summary>
		internal void SimulateLessEQ()
		{
			ZeroOne.Value pn2 = this.EvalStackPopWVal().NumericValue;
			ZeroOne.Value pn1 = this.EvalStackPopWVal().NumericValue;

			ZeroOne.Value res = ZeroOne.LogicalOr_Simulate(ZeroOne.Equal_Simulate(pn1, pn2), ZeroOne.Less_Simulate(pn1, pn2));
			this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, res);
		}

		/// <summary>
		/// Simulate the greater operation.
		/// </summary>
		internal void SimulateGreater()
		{
			ZeroOne.Value pn2 = this.EvalStackPopWVal().NumericValue;
			ZeroOne.Value pn1 = this.EvalStackPopWVal().NumericValue;

			ZeroOne.Value res = ZeroOne.Less_Simulate(pn2, pn1);
			this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, res);
		}

		/// <summary>
		/// Simulate the greater or equal operation.
		/// </summary>
		internal void SimulateGreaterEQ()
		{
			ZeroOne.Value pn2 = this.EvalStackPopWVal().NumericValue;
			ZeroOne.Value pn1 = this.EvalStackPopWVal().NumericValue;

			ZeroOne.Value res = ZeroOne.LogicalOr_Simulate(ZeroOne.Equal_Simulate(pn2, pn1), ZeroOne.Less_Simulate(pn2, pn1));
			this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, res);
		}

		//////////////
		//Primitive Arith Operations
		//and
		//Primitive Bitwise Operations

		/// <summary>
		/// Simulate an arbitrary and operation.
		/// </summary>
		internal void SimulateAnd()
		{
			ZeroOne.Value pn2 = this.EvalStackPopWVal().NumericValue;
			ZeroOne.Value pn1 = this.EvalStackPopWVal().NumericValue;

			ZeroOne.Value res = ZeroOne.LogicalAnd_Simulate(pn1, pn2);
			this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, res);
		}

		/// <summary>
		/// Simulate an arbitrary or operation.
		/// </summary>
		internal void SimulateOr()
		{
			ZeroOne.Value pn2 = this.EvalStackPopWVal().NumericValue;
			ZeroOne.Value pn1 = this.EvalStackPopWVal().NumericValue;

			ZeroOne.Value res = ZeroOne.LogicalOr_Simulate(pn1, pn2);
			this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, res);
		}

		/// <summary>
		/// Simulate an arbitrary binary operation.
		/// </summary>
		internal void SimulateUninterpBin()
		{
			this.EvalStackPop();
			IRNumericType resty = (IRNumericType)this.EvalStackPopWVal().SLocType;
			this.EvalStackPush(resty, ZeroOne.Value.Unknown);
		}

		/// <summary>
		/// Simulate an arbitrary unary operation.
		/// </summary>
		internal void SimulateUninterpUnary()
		{
			IRNumericType resty = (IRNumericType)this.EvalStackPopWVal().SLocType;
			this.EvalStackPush(resty, ZeroOne.Value.Unknown);
		}

		/// <summary>
		/// Analyze a conversion of one primitive type to another.
		/// </summary>
		internal void SimulateConvOp(IRNumericType cto)
		{
			Contract.Requires(cto != null);

			ZeroOne.Value pn = this.EvalStackPopWVal().NumericValue;
			this.EvalStackPush(cto, pn);
		}

		//////////////
		//Load/Store Through References

		/// <summary>
		/// Read a value from the array.
		/// </summary>
		internal void SimulateArrayLoad(int line, IRType loadtype)
		{
			this.EvalStackPop();
			APtrValueMap pref = this.EvalStackPopWVal().PointerValue;
			ZeroOne.Value prefnull = pref.PointerNullTest();
			if(prefnull == ZeroOne.Value.One)
			{
				this.SetInfeasable();
				return;
			}

			Nullable<APtrValueMap> pvm = null; 
			for(int i = 0; i < pref.PTargetCount; ++i)
			{
				APossiblePointerTarget prt = pref.PTargets[i];
				AObject rloc = this.ResolvePointerTarget(prt);

				IRMemberField cardf = ((IRContainerType)rloc.LocationType).CardField;
				IRBasicAccessPath cardp = GlobalAnalysisState.TProg.GetAccessPathForSingleField(cardf);
				rloc.DoGeneralReadFromLocation(cardp, line);

				IRMemberField contf = ((IRContainerType)rloc.LocationType).ContentsField;
				IRBasicAccessPath contp = GlobalAnalysisState.TProg.GetAccessPathForSingleField(contf);
				Nullable<APtrValueMap> tpm = rloc.DoGeneralReadFromLocation(contp, line);

				if(tpm.HasValue)
				{
					if(!pvm.HasValue)
						pvm = tpm.Value;
					else
						pvm = APtrValueMap.MergeAPtrMaps(pvm.Value, tpm.Value, false, true);
				}
			}

			if(loadtype is IRNumericType)
				this.EvalStackPush((IRNumericType)loadtype, ZeroOne.Value.Unknown);
			else if(loadtype is IREnumType)
				this.EvalStackPush(((IREnumType)loadtype).UnerlyingNumericType, ZeroOne.Value.Unknown);
			else if(loadtype is IRStructType)
				this.EvalStackPush((IRStructType)loadtype, pvm.Value);
			else
				this.EvalStackPush((IRPtrType)loadtype, pvm.Value);
		}

		/// <summary>
		/// Store a value into the array.
		/// </summary>
		internal void SimulateArrayStore(int line, IRType storetype)
		{
			AEvalStackEntry vsv = this.EvalStackPopWVal();
			this.EvalStackPop();
			APtrValueMap pref = this.EvalStackPopWVal().PointerValue;
			ZeroOne.Value prefnull = pref.PointerNullTest();
			if(prefnull == ZeroOne.Value.One)
			{
				this.SetInfeasable();
				return;
			}

			for(int i = 0; i < pref.PTargetCount; ++i)
			{
				APossiblePointerTarget pt = pref.PTargets[i];
				AContainer storeloc = (AContainer)this.ResolvePointerTarget(pt);

				IRMemberField cardf = ((IRContainerType)storeloc.LocationType).CardField;
				IRBasicAccessPath cardp = GlobalAnalysisState.TProg.GetAccessPathForSingleField(cardf);
				storeloc.DoGeneralReadFromLocation(cardp, line);

				APtrValueMap pvm = default(APtrValueMap);
				if(vsv.SLocType is IRPtrType)
				{
					Contract.Assert(IRProgram.IsT1AssignableToT2(vsv.SLocType, storetype));
					pvm = vsv.PointerValue;
				}
				else if(vsv.SLocType is IRStructType)
				{
					Contract.Assert(IRProgram.IsT1AssignableToT2(vsv.SLocType, storetype));
					pvm = vsv.StructValue;
				}
				else
				{
					;
				}

				IRMemberField contf = ((IRContainerType)storeloc.LocationType).ContentsField;
				IRBasicAccessPath contp = GlobalAnalysisState.TProg.GetAccessPathForSingleField(contf);
				storeloc.DoContainerContentsWriteToLocationBI(contp, pvm, line, null);
			}
		}

		/// <summary>
		/// Get the length of the array.
		/// </summary>
		internal void SimulateArrayLength(int line)
		{
			APtrValueMap pref = this.EvalStackPopWVal().PointerValue;
			ZeroOne.Value prefnull = pref.PointerNullTest();
			if(prefnull == ZeroOne.Value.One)
			{
				this.SetInfeasable();
				return;
			}

			for(int i = 0; i < pref.PTargetCount; ++i)
			{
				APossiblePointerTarget prt = pref.PTargets[i];
				AObject rloc = this.ResolvePointerTarget(prt);

				IRMemberField cardf = ((IRContainerType)rloc.LocationType).CardField;
				IRBasicAccessPath cardp = GlobalAnalysisState.TProg.GetAccessPathForSingleField(cardf);
				rloc.DoGeneralReadFromLocation(cardp, line);
			}

			this.EvalStackPush((IRNumericType)GlobalAnalysisState.TProg.TypeTable.Int64Type, ZeroOne.Value.Unknown);
		}

		/// <summary>
		/// Read a value through the Reference.
		/// </summary>
		internal void SimulateDeRefIndirectRead(int line)
		{
			AReference vref = this.EvalStackPopWVal().ReferenceValue;
			ZeroOne.Value vrefnull = vref.ReferenceNullTest();
			if(vrefnull == ZeroOne.Value.One)
			{
				this.SetInfeasable();
				return;
			}
			
			IRType trgttype = vref.ReferenceType.ReferenceTargetType;
			Nullable<APtrValueMap> pvm = null;
			for(int i = 0; i < vref.RTargetCount; ++i)
			{
				APossibleReferenceTarget prt = vref.GetIthPossibleRefTrgt(i);
				ALocation rloc = this.ResolveReferenceTarget(prt);
				Nullable<APtrValueMap> tpp = rloc.DoGeneralReadFromLocation(prt.TrgtOffset, line);

				if(tpp.HasValue)
				{
					if(!pvm.HasValue)
						pvm = tpp;
					else
						pvm = APtrValueMap.MergeAPtrMaps(pvm.Value, tpp.Value, false, true);
				}
			}

			if(trgttype is IRNumericType)
				this.EvalStackPush((IRNumericType)trgttype, ZeroOne.Value.Unknown);
			else if(trgttype is IREnumType)
				this.EvalStackPush(((IREnumType)trgttype).UnerlyingNumericType, ZeroOne.Value.Unknown);
			else if(trgttype is IRPtrType)
				this.EvalStackPush((IRPtrType)trgttype, pvm.Value);
			else
				this.EvalStackPush((IRStructType)trgttype, pvm.Value);
		}

		/// <summary>
		/// Store a value through the reference.
		/// </summary>
		internal void SimulateDeRefIndirectWrite(int line)
		{
			AEvalStackEntry vsv = this.EvalStackPopWVal();
			AReference vref = this.EvalStackPopWVal().ReferenceValue;
			ZeroOne.Value vrefnull = vref.ReferenceNullTest();
			if(vrefnull == ZeroOne.Value.One)
			{
				this.SetInfeasable();
				return;
			}

			IRType storetype = vref.ReferenceType.ReferenceTargetType;
			for(int i = 0; i < vref.RTargetCount; ++i)
			{
				APossibleReferenceTarget aprt = vref.GetIthPossibleRefTrgt(i);
				ALocation storeloc = this.ResolveReferenceTarget(aprt);

				APtrValueMap appt = default(APtrValueMap);
				if(vsv.SLocType is IRPtrType)
				{
					Contract.Assert(IRProgram.IsT1AssignableToT2(vsv.SLocType, storetype));
					appt = vsv.PointerValue;
				}
				else if(vsv.SLocType is IRStructType)
				{
					Contract.Assert(IRProgram.IsT1AssignableToT2(vsv.SLocType, storetype));
					appt = vsv.StructValue;
				}
				else
				{
					;
				}

				storeloc.DoGeneralWriteToLocation(aprt.TrgtOffset, appt, vref.RTargetCount == 1, line);
			}
		}

		/// <summary>
		/// Initialize a struct/class value through the reference.
		/// </summary>
		internal void SimulateDeRefIndirectInitialize(IRType toinit, int line)
		{
			AReference vref = this.EvalStackPopWVal().ReferenceValue;
			Contract.Assert(vref.ReferenceType.ReferenceTargetType == toinit);

			ZeroOne.Value vrefnull = vref.ReferenceNullTest();
			if(vrefnull == ZeroOne.Value.One)
			{
				this.SetInfeasable();
				return;
			}

			for(int i = 0; i < vref.RTargetCount; ++i)
			{
				APossibleReferenceTarget aprt = vref.GetIthPossibleRefTrgt(i);
				ALocation storeloc = this.ResolveReferenceTarget(aprt);

				APtrValueMap ppvm = APtrValueMap.MakeInitalPtrValueMapComposite(toinit.TypeDescription.AllTerminalAccessPaths);
				storeloc.DoGeneralWriteToLocation(aprt.TrgtOffset, ppvm, vref.RTargetCount == 1, line);
			}
		}

		/// <summary>
		/// Do a load from a struct on the evaluation stack.
		/// </summary>
		internal void SimulateReadFromStructOnStack(IRMemberField mf, int line)
		{
			AEvalStackEntry sstr = this.EvalStackPopWVal();
			
			IRType trgttype = mf.FieldType;
			IRBasicAccessPath mfp = GlobalAnalysisState.TProg.GetAccessPathForSingleField(mf);

			if(trgttype is IRNumericType)
			{
				this.EvalStackPush((IRNumericType)trgttype, ZeroOne.Value.Unknown);
			}
			else if(trgttype is IREnumType)
			{
				this.EvalStackPush(((IREnumType)trgttype).UnerlyingNumericType, ZeroOne.Value.Unknown);
			}
			else if(trgttype is IRPtrType)
			{
				APtrValueMap pvm = sstr.PointerValue.ReadPtrValues(mfp);
				this.EvalStackPush((IRPtrType)trgttype, pvm);
			}
			else
			{
				APtrValueMap pvm = sstr.StructValue.ReadPtrValues(mfp);
				this.EvalStackPush((IRStructType)trgttype, pvm);
			}
		}

		//////////////
		//Pointer Creation and Indexing

		/// <summary>
		/// Load the address of a local variable.
		/// </summary>
		internal void SimulateLoadLocalAddr(IRVarName rv)
		{
			Contract.Requires(rv != null);

			AHomeLocation lhv = this.ResolveLocalGlobalTarget(rv);
			IRReferenceType reftype = GlobalAnalysisState.TProg.TypeTable.LookupReferenceTypeFor(lhv.LocationType);
			AReference erv = new AReference(reftype, new APossibleReferenceTarget(lhv.Address, IRBasicAccessPath.EmptyAccessPath));
			this.EvalStackPush(reftype, erv);
		}

		/// <summary>
		/// Load the address of a global address.
		/// </summary>
		internal void SimulateLoadGlobalAddr(IRStaticField sf)
		{
			Contract.Requires(sf != null);

			AHomeLocation lhv = this.ResolveLocalGlobalTarget(sf);
			IRReferenceType reftype = GlobalAnalysisState.TProg.TypeTable.LookupReferenceTypeFor(lhv.LocationType);
			AReference erv = new AReference(reftype, new APossibleReferenceTarget(lhv.Address, IRBasicAccessPath.EmptyAccessPath));
			this.EvalStackPush(reftype, erv);
		}

		/// <summary>
		/// Index a pointer by the given member field, also take the position on the stack of the pointer (0 is the top element).
		/// </summary>
		internal void SimulateIndexAddrByField(IRMemberField mf, int sloc)
		{
			Contract.Requires(mf != null);
			Contract.Assert((0 <= sloc) & (sloc < this.m_evalstack.Count));

			AEvalStackEntry evse = this.m_evalstack[this.m_evalstack.Count - (sloc + 1)];
			AReference vref;
			if(evse.SLocType is IRReferenceType)
			{
				vref = evse.ReferenceValue;
				ZeroOne.Value vrefnull = vref.ReferenceNullTest();
				if(vrefnull == ZeroOne.Value.One)
				{
					this.SetInfeasable();
					return;
				}
			}
			else
			{
				if(evse.PointerValue.PTargetCount == 0)
				{
					this.SetInfeasable();
					return;
				}

				Contract.Assert(Contract.ForAll(evse.PointerValue.PTargets, (APossiblePointerTarget aprt) => this.ResolvePointerTarget(aprt).LocationType.TypeDescription.AllVisibleFields.Contains(mf)), "We have a typing problem.");
				
				IRReferenceType rft = GlobalAnalysisState.TProg.TypeTable.LookupReferenceTypeFor(mf.FieldType);
				vref = AReference.ConvertToReference(rft, evse.PointerValue.PTargets, evse.PointerValue.PathMustNonNull(IRBasicAccessPath.EmptyAccessPath));
			}

			AReference idxr = vref.IndexAddrByFieldOrIndex(mf);
			this.m_evalstack[this.m_evalstack.Count - (sloc + 1)] = AEvalStackEntry.MakeReferenceStackEntry(idxr.ReferenceType, idxr);
		}

		/// <summary>
		/// Index a pointer by the given member field, also take the position on the stack of the pointer (0 is the top element).
		/// </summary>
		internal void SimulateIndexAddrInsideArray(IRMemberField mf)
		{
			this.EvalStackPop();
			APtrValueMap pref = this.EvalStackPopWVal().PointerValue;
			if(pref.PTargetCount == 0)
			{
				this.SetInfeasable();
				return;
			}

			Contract.Assert(Contract.ForAll(pref.PTargets, (APossiblePointerTarget aprt) => ((IRContainerType)this.ResolvePointerTarget(aprt).LocationType).ContentsField == mf), "We have a typing problem.");

			IRReferenceType rft = GlobalAnalysisState.TProg.TypeTable.LookupReferenceTypeFor(mf.FieldType);
			AReference vref = AReference.ConvertToReference(rft, pref.PTargets, pref.PathMustNonNull(IRBasicAccessPath.EmptyAccessPath));	
			AReference idxr = vref.IndexAddrByFieldOrIndex(mf);
			this.EvalStackPush(vref.ReferenceType, idxr);
		}

		/// <summary>
		/// Simulate the load of a known function pointer to the stack.
		/// </summary>
		internal void SimulateLoadFuncPtr(IRInvokeIdentity invid)
		{
			AEvalStackEntry fpv = AEvalStackEntry.MakeFunctionPtrStackEntry(GlobalAnalysisState.TProg.TypeTable.FunctionPtrType, invid);
			this.EvalStackPush(fpv);
		}

		//////////////
		//Pointer Compare

		/// <summary>
		/// Equality of the references or pointers on top of the stack.
		/// </summary>
		internal void SimulateDrefableEQ()
		{
			if(this.EvalStackPeek().SLocType is IRPtrType)
			{
				APtrValueMap p1 = this.EvalStackPopWVal().PointerValue;
				APtrValueMap p2 = this.EvalStackPopWVal().PointerValue;

				ZeroOne.Value rv = APtrValueMap.PointerEqualsTest(p1, p2);
				this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, rv);
			}
			else
			{
				AReference r1 = this.EvalStackPopWVal().ReferenceValue;
				AReference r2 = this.EvalStackPopWVal().ReferenceValue;

				ZeroOne.Value rv = AReference.ReferenceEqualsTest(r1, r2);
				this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, rv);
			}
		}

		/// <summary>
		/// Is the pointer on top of the stack non-null.
		/// </summary>
		internal void SimulatePointerNonNull()
		{
			if(this.EvalStackPeek().SLocType is IRPtrType)
			{
				APtrValueMap p = this.EvalStackPopWVal().PointerValue;
				ZeroOne.Value rv = ZeroOne.LogicalNot_Simulate(p.PointerNullTest());
				this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, rv);
			}
			else
			{
				AReference r = this.EvalStackPopWVal().ReferenceValue;
				ZeroOne.Value rv = ZeroOne.LogicalNot_Simulate(r.ReferenceNullTest());
				this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, rv);
			}
		}

		/// <summary>
		/// Is the reciver value in a vcall non-null.
		/// </summary>
		internal bool IsVCallNonNull(int rcvrpos)
		{
			AEvalStackEntry evse = this.m_evalstack[this.m_evalstack.Count - rcvrpos];

			if(evse.SLocType is IRPtrType)
				return evse.PointerValue.PTargetCount != 0;
			else if(evse.SLocType is IRReferenceType)
				return evse.ReferenceValue.RTargetCount != 0;
			else
				return true;
		}

		/// <summary>
		/// Is the reciver value in a vcall non-null.
		/// </summary>
		internal void AssertVCallTargetNonNull(int rcvrpos)
		{
			AEvalStackEntry evse = this.m_evalstack[this.m_evalstack.Count - rcvrpos];

			if(evse.SLocType is IRPtrType)
			{
				APtrValueMap p = evse.PointerValue;
				this.m_evalstack[this.m_evalstack.Count - rcvrpos] = AEvalStackEntry.MakePtrStackEntry((IRPtrType)evse.SLocType, p.AssertTargetNonNull());
			}
			else if(evse.SLocType is IRReferenceType)
			{
				AReference r = evse.ReferenceValue;
				this.m_evalstack[this.m_evalstack.Count - rcvrpos] = AEvalStackEntry.MakeReferenceStackEntry((IRReferenceType)evse.SLocType, r.AssertTargetNonNull());
			}
			else
			{
				;
			}
		}

		//////////////
		//Type Operations

		/// <summary>
		/// Box the valuetype on the top of the stack.
		/// </summary>
		internal void SimulateBox(IRValueType typetobox, int line)
		{
			Contract.Requires(typetobox != null);

			IRBoxedType boxedty = GlobalAnalysisState.TProg.TypeTable.LookupBoxedTypeFor(typetobox);
			IRPtrType ptrtoboxedty = GlobalAnalysisState.TProg.TypeTable.LookupPointerTypeFor(boxedty);
			IRReferenceType reftoboxedty = GlobalAnalysisState.TProg.TypeTable.LookupReferenceTypeFor(boxedty);

			AObject bxn = AObject.AllocateObjectOfType(this.m_memory, boxedty, line);
			IRMemberField boxf = boxedty.BoxedValueField;
			IRBasicAccessPath boxbap = GlobalAnalysisState.TProg.GetAccessPathForSingleField(boxf);
			
			AReference refv = new AReference(GlobalAnalysisState.TProg.TypeTable.LookupReferenceTypeFor(typetobox), new APossibleReferenceTarget(bxn.Address, boxbap));

			AEvalStackEntry vv = this.EvalStackPopWVal();
			this.EvalStackPush(ptrtoboxedty, APtrValueMap.MakePtrWSingleTarget(new APossiblePointerTarget(bxn.Address), true));
			this.EvalStackPush(refv.ReferenceType, refv);
			this.EvalStackPush(vv);
			this.SimulateDeRefIndirectWrite(line);
		}

		/// <summary>
		/// Unbox the boxed object on that hte offset from the stack top (e.g. get a pointer to the boxed contents).
		/// </summary>
		internal void SimulateUnBox(IRValueType typetounbox, int sloc)
		{
			Contract.Requires(typetounbox != null);

			int ssloc = (sloc == -1 ? (this.m_evalstack.Count - 1) : sloc);
			AEvalStackEntry sn = this.m_evalstack[ssloc];
			APtrValueMap pp = sn.PointerValue;

			ZeroOne.Value isnull = pp.PointerNullTest();
			if(isnull == ZeroOne.Value.One)
			{
				DebugReport.ReportError("Unbox of null reference, we should fix this for nullable types at some point in time.");
				throw new InvalidOperationException();
			}

			IRBoxedType boxetype = GlobalAnalysisState.TProg.TypeTable.LookupBoxedTypeFor(typetounbox);
			IRMemberField boxfield = boxetype.BoxedValueField;

			AReference rr = AReference.ConvertToReference(GlobalAnalysisState.TProg.TypeTable.LookupReferenceTypeFor(typetounbox), pp.PTargets, true);
			AReference tocontents = rr.IndexAddrByFieldOrIndex(boxfield);
			this.m_evalstack[ssloc] = AEvalStackEntry.MakeReferenceStackEntry(rr.ReferenceType, tocontents);
		}

		/// <summary>
		/// Cast with throw to given type.
		/// </summary>
		internal void SimulateCast(IRPtrType castto, int line)
		{
			Contract.Requires(castto != null);

			bool isinst = this.CheckIsInstOfStackTop(castto, true, line);
			if(!isinst)
				this.SetInfeasable();
		}

		/// <summary>
		/// Cast without throw to given type (null is pushed if not possible otherwise the recast pointer is).
		/// </summary>
		internal void SimulateIsInst(IRPtrType instof, int line)
		{
			Contract.Requires(instof != null);

			this.CheckIsInstOfStackTop(instof, false, line);
		}

		/// <summary>
		/// Perform the constraint operation on the given stack position.
		/// </summary>
		internal void SimulateConstrain(IRType constrinto, int pos, int line)
		{
			Contract.Requires(constrinto != null);

			AEvalStackEntry evse = this.m_evalstack[this.m_evalstack.Count - (pos + 1)];
			this.EvalStackPush(evse);

			if(constrinto is IRReferenceType)
			{ ;}
			else
			{
				Contract.Assert(constrinto is IRPtrType);

				IRType atype = ((IRPtrType)constrinto).PtrTargetType;
				if(atype is IRBoxedType)
				{
					this.SimulateDeRefIndirectRead(line);
					this.SimulateBox(((IRBoxedType)atype).BoxedTypeValue, line);
				}
				else
				{
					this.SimulateDeRefIndirectRead(line);
				}
			}

			AEvalStackEntry constr = this.EvalStackPopWVal();
			this.m_evalstack[this.m_evalstack.Count - (pos + 1)] = constr;
		}

		/// <summary>
		/// return true if the top value on the stack is a subtype of the given derefable (treats a null pointer as a subtype if 
		/// <c>nulloksubtype</c> is true otherwise null is not a subtype of any type).
		/// </summary>
		private bool CheckIsInstOfStackTop(IRPtrType instof, bool nulloksubtype, int line)
		{
			APtrValueMap pn = this.EvalStackPopWVal().PointerValue;
			ZeroOne.Value nv = pn.PointerNullTest();

			if(nv == ZeroOne.Value.One)
			{
				this.EvalStackPush(instof, APtrValueMap.MakeInitalPtrValueMapPtr());
				return nulloksubtype;
			}

			bool anyok = false;
			List<APossiblePointerTarget> app = new List<APossiblePointerTarget>();
			for(int i = 0; i < pn.PTargetCount; ++i)
			{
				APossiblePointerTarget ppt = pn.PTargets[i];
				AObject ploc = this.ResolvePointerTarget(ppt);

				//simulate read from type tag
				ploc.MarkRTTIUsed(line);

				bool ok = instof.PtrTargetType.TypeDescription.AllSubTypes.Contains(ploc.ObjectType);
				anyok |= ok;

				if(ok)
					app.Add(ppt);
			}

			APossiblePointerTarget[] nap = (app.Count == 0 ? APtrValueMap.EmptyTargetMap : app.ToArray());
			this.EvalStackPush(instof, APtrValueMap.MakePtrPostCheckIsInst(nap));

			return anyok;
		}

		/// <summary>
		/// Convert a pointer to a reference.
		/// </summary>
		internal void SimulateConvToReference(int argoffset, IRReferenceType reftype)
		{
			Contract.Requires(reftype != null);

			int spos = this.m_evalstack.Count - (argoffset + 1);
			AEvalStackEntry sn = this.m_evalstack[spos];
			Contract.Assert(sn.SLocType is IRPtrType);

			//change the type of the SLoc
			IRReferenceType nrt = GlobalAnalysisState.TProg.TypeTable.LookupReferenceTypeFor(((IRPtrType)sn.SLocType).PtrTargetType);
			AReference rr = AReference.ConvertToReference(nrt, sn.PointerValue.PTargets, sn.PointerValue.PathMustNonNull(IRBasicAccessPath.EmptyAccessPath));
			this.m_evalstack[spos] = AEvalStackEntry.MakeReferenceStackEntry(rr.ReferenceType, rr);
		}

		//////////////
		//Misc Operations

		/// <summary>
		/// Pop the top of the stack.
		/// </summary>
		internal void SimulatePop()
		{
			this.EvalStackPop();
		}

		/// <summary>
		/// Duplicate the element on the top of the stack.
		/// </summary>
		internal void SimulateDup()
		{
			AEvalStackEntry sn = this.EvalStackPeek();
			this.EvalStackPush(sn);
		}

		/// <summary>
		///Push the null literal on the stack.
		/// </summary>
		internal void SimulatePushNull()
		{
			AEvalStackEntry ee = AEvalStackEntry.MakePtrStackEntry(GlobalAnalysisState.TProg.TypeTable.NullType, APtrValueMap.MakeInitalPtrValueMapPtr());
			this.EvalStackPush(ee);
		}

		/// <summary>
		/// Push the given int literal on the stack.
		/// </summary>
		internal void SimulatePushInt(long val)
		{
			ZeroOne.Value vv = ZeroOne.IntToValue(val);
			this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Int64Type, vv);
		}

		/// <summary>
		/// Push the given float literal on the stack.
		/// </summary>
		internal void SimulatePushFloat(double fval)
		{
			this.EvalStackPush(GlobalAnalysisState.TProg.TypeTable.Float64Type, ZeroOne.Value.Unknown);
		}

		/// <summary>
		/// Push the given string literal on the stack.
		/// </summary>
		internal void SimulatePushString(int line)
		{
			AObject sloc = AObject.AllocateObjectOfType(this.m_memory, GlobalAnalysisState.TProg.TypeTable.StringObjectType, line);
			IRPtrType sptr = GlobalAnalysisState.TProg.TypeTable.LookupPointerTypeFor(GlobalAnalysisState.TProg.TypeTable.StringObjectType);
			this.EvalStackPush(sptr, new APossiblePointerTarget(sloc.Address), true);
		}

		////////
		//Support for calls

		/// <summary>
		/// Assert that an argument parameter var is of a specific type.
		/// </summary>
		internal void SetArgType(IRType tt, int argpos)
		{
			Contract.Requires(tt != null);

			if(this.m_evalstack[argpos].SLocType is IRPtrType)
				this.m_evalstack[argpos] = AEvalStackEntry.MakePtrStackEntry((IRPtrType)tt, this.m_evalstack[argpos].PointerValue);
		}

		/// <summary>
		/// Return the type of the eval stack that the call is being invoked on.
		/// </summary>
		internal IRType GetTargetEvalStackRcvrType(int rcvrpos)
		{
			return this.m_evalstack[this.m_evalstack.Count - rcvrpos].SLocType;
		}

		/// <summary>
		/// Return the resolved method target for a virtual call.
		/// </summary>
		internal IRClassType GetTargetCallClassForName(int rcvrpos, int line)
		{
			APtrValueMap pn = this.m_evalstack[rcvrpos].PointerValue;
			Contract.Assert(pn.PTargetCount == 1, "This should be set as a unique value ealier.");

			AObject obj = this.ResolvePointerTarget(pn.PTargets[0]);

			obj.MarkRTTIUsed(line);
			return (IRClassType)obj.LocationType;
		}

		/// <summary>
		/// When making recursive calls we merge things aggressively -- but this means we could merge multiple home locations.
		/// To avoid these issues we just assert that recursive calls never involve reference parameters.
		/// </summary>
		internal void CheckByRefFreeForRecCalls()
		{
#if DEBUG
			Contract.Assert(this.m_evalstack.Count == 0);
			foreach(IRRootIdentifier rr in this.m_nametonodemap.Keys)
			{
				ALocation ll = this.ResolveLocalGlobalTarget(rr);
				Contract.Assert(!(ll.LocationType is IRReferenceType)); 
			}
#endif
		}
	}
}
